\begin{tabbing}
$M$:$k$ may not read $x$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fpf{-}dom(IdDeq; $x$; (($M$.2.2.2.2.2.2.2.2.2.2).1))\+
\\[0ex]$\wedge_{b}$ ($\neg_{b}$deq{-}member(KindDeq;$k$;($M$.2.2.2.2.2.2.2.2.2.2).1IdDeq($x$)))
\-
\end{tabbing}